es:ES, ff:FIFO.
rcvr:j,i:ff.C{e:E| ff.S(j,i,e)} {e:E| ff.R(i,e)} 
(j, i:ff.C, e:{e:E| ff.S(j,i,e)} . ff.Sender(i,rcvr(j,i,e)) = e) 

latex

Definitions	x:A. B(x), t  T, x:A. B(x), , t.1, P  Q, Q  f P, P & Q, Q f P, A c B
Lemmas	FIFO wf, event system wf, fifoSender-antecedent, es-E wf, fifoS wf, fifoC wf, fifoSender wf, fifoR wf